Left Termination of the query pattern
palindrome(g)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

palindrome(Xs) :- reverse(Xs, Xs).
reverse(X1s, X2s) :- reverse(X1s, [], X2s).
reverse([], Xs, Xs).
reverse(.(X, X1s), X2s, Ys) :- reverse(X1s, .(X, X2s), Ys).

Query: palindrome(g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="B: palindrome(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: palindrome(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: reverse(T3, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: reverse(T3, T3), SCOPE: 2, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: reverse(T6, [], T6)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: reverse(T6, [], T6), SCOPE: 3, CLAUSE: 2 | reverse(T6, [], T6), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: reverse(T6, [], T6), SCOPE: 3, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: reverse(T6, [], T6), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: reverse(T12, .(T11, []), .(T11, T12))\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 2 | reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 2\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27)))\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 2 | reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 3\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 2\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 3\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52))))\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 2 | reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 3\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 2\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 3\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87)))))\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 2 | reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 3\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 2\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 3\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132))))))\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 2 | reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 3\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 2\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 3\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187)))))))\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 2 | reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 2\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252))))))))\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 2 | reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 3\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 2\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 3\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: reverse(T327, .(T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, [])))))))), .(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))\n\nT326 is ground\nT327 is ground\nT328 is ground\nT329 is ground\nT330 is ground\nT331 is ground\nT332 is ground\nT333 is ground\nT334 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="A: reverse(T327, .(T326, T351), .(T334, T352))\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 2 | reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 3\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 2\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 3\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: reverse(T380, .(T379, .(T381, T382)), .(T383, T384))\n\nT379 is ground\nT380 is ground\nT381 is ground\nT382 is ground\nT383 is ground\nT384 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 79 [arrowhead = none ];
79 -> 2;

80 [label="ONLY EVAL with clause\npalindrome(X2) :- reverse(X2, X2).\nand substitutionT1 -> T3,\nX2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 80 [arrowhead = none ];
80 -> 3;

81 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 81 [arrowhead = none ];
81 -> 4;

82 [label="ONLY EVAL with clause\nreverse(X9, X10) :- reverse(X9, [], X10).\nand substitutionT3 -> T6,\nX9 -> T6,\nX10 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 82 [arrowhead = none ];
82 -> 5;

83 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 83 [arrowhead = none ];
83 -> 6;

84 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 84 [arrowhead = none ];
84 -> 7;

85 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 85 [arrowhead = none ];
85 -> 8;

86 [label="EVAL with clause\nreverse([], X17, X17).\nand substitutionT6 -> [],\nX17 -> []", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 86 [arrowhead = none ];
86 -> 9;

87 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 87 [arrowhead = none ];
87 -> 10;

88 [label="EVAL with clause\nreverse(.(X26, X27), X28, X29) :- reverse(X27, .(X26, X28), X29).\nand substitutionX26 -> T11,\nX27 -> T12,\nT6 -> .(T11, T12),\nX28 -> [],\nX29 -> .(T11, T12)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 88 [arrowhead = none ];
88 -> 12;

89 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 89 [arrowhead = none ];
89 -> 13;

90 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 90 [arrowhead = none ];
90 -> 11;

91 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 91 [arrowhead = none ];
91 -> 14;

92 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 92 [arrowhead = none ];
92 -> 15;

93 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 93 [arrowhead = none ];
93 -> 16;

94 [label="EVAL with clause\nreverse([], X36, X36).\nand substitutionT12 -> [],\nT11 -> T19,\nX36 -> .(T19, [])", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 94 [arrowhead = none ];
94 -> 17;

95 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 95 [arrowhead = none ];
95 -> 18;

96 [label="EVAL with clause\nreverse(.(X45, X46), X47, X48) :- reverse(X46, .(X45, X47), X48).\nand substitutionX45 -> T26,\nX46 -> T27,\nT12 -> .(T26, T27),\nT11 -> T28,\nX47 -> .(T28, []),\nX48 -> .(T28, .(T26, T27))", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 96 [arrowhead = none ];
96 -> 20;

97 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 97 [arrowhead = none ];
97 -> 21;

98 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 98 [arrowhead = none ];
98 -> 19;

99 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
20 -> 99 [arrowhead = none ];
99 -> 22;

100 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
22 -> 100 [arrowhead = none ];
100 -> 23;

101 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
22 -> 101 [arrowhead = none ];
101 -> 24;

102 [label="EVAL with clause\nreverse([], X55, X55).\nand substitutionT27 -> [],\nT26 -> T42,\nT28 -> T42,\nX55 -> .(T42, .(T42, [])),\nT41 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 102 [arrowhead = none ];
102 -> 25;

103 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 103 [arrowhead = none ];
103 -> 26;

104 [label="EVAL with clause\nreverse(.(X64, X65), X66, X67) :- reverse(X65, .(X64, X66), X67).\nand substitutionX64 -> T51,\nX65 -> T52,\nT27 -> .(T51, T52),\nT26 -> T53,\nT28 -> T54,\nX66 -> .(T53, .(T54, [])),\nX67 -> .(T54, .(T53, .(T51, T52)))", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 104 [arrowhead = none ];
104 -> 28;

105 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 105 [arrowhead = none ];
105 -> 29;

106 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 106 [arrowhead = none ];
106 -> 27;

107 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
28 -> 107 [arrowhead = none ];
107 -> 30;

108 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 108 [arrowhead = none ];
108 -> 31;

109 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 109 [arrowhead = none ];
109 -> 32;

110 [label="EVAL with clause\nreverse([], X74, X74).\nand substitutionT52 -> [],\nT51 -> T75,\nT53 -> T74,\nT54 -> T75,\nX74 -> .(T75, .(T74, .(T75, []))),\nT73 -> T75", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 110 [arrowhead = none ];
110 -> 33;

111 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 111 [arrowhead = none ];
111 -> 34;

112 [label="EVAL with clause\nreverse(.(X83, X84), X85, X86) :- reverse(X84, .(X83, X85), X86).\nand substitutionX83 -> T86,\nX84 -> T87,\nT52 -> .(T86, T87),\nT51 -> T88,\nT53 -> T89,\nT54 -> T90,\nX85 -> .(T88, .(T89, .(T90, []))),\nX86 -> .(T90, .(T89, .(T88, .(T86, T87))))", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 112 [arrowhead = none ];
112 -> 36;

113 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 113 [arrowhead = none ];
113 -> 37;

114 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 114 [arrowhead = none ];
114 -> 35;

115 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
36 -> 115 [arrowhead = none ];
115 -> 38;

116 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
38 -> 116 [arrowhead = none ];
116 -> 39;

117 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
38 -> 117 [arrowhead = none ];
117 -> 40;

118 [label="EVAL with clause\nreverse([], X93, X93).\nand substitutionT87 -> [],\nT86 -> T118,\nT88 -> T117,\nT89 -> T117,\nT90 -> T118,\nX93 -> .(T118, .(T117, .(T117, .(T118, [])))),\nT115 -> T118,\nT116 -> T117", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 118 [arrowhead = none ];
118 -> 41;

119 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 119 [arrowhead = none ];
119 -> 42;

120 [label="EVAL with clause\nreverse(.(X102, X103), X104, X105) :- reverse(X103, .(X102, X104), X105).\nand substitutionX102 -> T131,\nX103 -> T132,\nT87 -> .(T131, T132),\nT86 -> T133,\nT88 -> T134,\nT89 -> T135,\nT90 -> T136,\nX104 -> .(T133, .(T134, .(T135, .(T136, [])))),\nX105 -> .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 120 [arrowhead = none ];
120 -> 44;

121 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 121 [arrowhead = none ];
121 -> 45;

122 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 122 [arrowhead = none ];
122 -> 43;

123 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
44 -> 123 [arrowhead = none ];
123 -> 46;

124 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 124 [arrowhead = none ];
124 -> 47;

125 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 125 [arrowhead = none ];
125 -> 48;

126 [label="EVAL with clause\nreverse([], X112, X112).\nand substitutionT132 -> [],\nT131 -> T171,\nT133 -> T170,\nT134 -> T169,\nT135 -> T170,\nT136 -> T171,\nX112 -> .(T171, .(T170, .(T169, .(T170, .(T171, []))))),\nT167 -> T171,\nT168 -> T170", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 126 [arrowhead = none ];
126 -> 49;

127 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 127 [arrowhead = none ];
127 -> 50;

128 [label="EVAL with clause\nreverse(.(X121, X122), X123, X124) :- reverse(X122, .(X121, X123), X124).\nand substitutionX121 -> T186,\nX122 -> T187,\nT132 -> .(T186, T187),\nT131 -> T188,\nT133 -> T189,\nT134 -> T190,\nT135 -> T191,\nT136 -> T192,\nX123 -> .(T188, .(T189, .(T190, .(T191, .(T192, []))))),\nX124 -> .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 128 [arrowhead = none ];
128 -> 52;

129 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 129 [arrowhead = none ];
129 -> 53;

130 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 130 [arrowhead = none ];
130 -> 51;

131 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
52 -> 131 [arrowhead = none ];
131 -> 54;

132 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 132 [arrowhead = none ];
132 -> 55;

133 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 133 [arrowhead = none ];
133 -> 56;

134 [label="EVAL with clause\nreverse([], X131, X131).\nand substitutionT187 -> [],\nT186 -> T234,\nT188 -> T233,\nT189 -> T232,\nT190 -> T232,\nT191 -> T233,\nT192 -> T234,\nX131 -> .(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))),\nT229 -> T234,\nT230 -> T233,\nT231 -> T232", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 134 [arrowhead = none ];
134 -> 57;

135 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 135 [arrowhead = none ];
135 -> 58;

136 [label="EVAL with clause\nreverse(.(X140, X141), X142, X143) :- reverse(X141, .(X140, X142), X143).\nand substitutionX140 -> T251,\nX141 -> T252,\nT187 -> .(T251, T252),\nT186 -> T253,\nT188 -> T254,\nT189 -> T255,\nT190 -> T256,\nT191 -> T257,\nT192 -> T258,\nX142 -> .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, [])))))),\nX143 -> .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 136 [arrowhead = none ];
136 -> 60;

137 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 137 [arrowhead = none ];
137 -> 61;

138 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 138 [arrowhead = none ];
138 -> 59;

139 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
60 -> 139 [arrowhead = none ];
139 -> 62;

140 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 140 [arrowhead = none ];
140 -> 63;

141 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 141 [arrowhead = none ];
141 -> 64;

142 [label="EVAL with clause\nreverse([], X150, X150).\nand substitutionT252 -> [],\nT251 -> T307,\nT253 -> T306,\nT254 -> T305,\nT255 -> T304,\nT256 -> T305,\nT257 -> T306,\nT258 -> T307,\nX150 -> .(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))),\nT301 -> T307,\nT302 -> T306,\nT303 -> T305", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 142 [arrowhead = none ];
142 -> 65;

143 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 143 [arrowhead = none ];
143 -> 66;

144 [label="EVAL with clause\nreverse(.(X159, X160), X161, X162) :- reverse(X160, .(X159, X161), X162).\nand substitutionX159 -> T326,\nX160 -> T327,\nT252 -> .(T326, T327),\nT251 -> T328,\nT253 -> T329,\nT254 -> T330,\nT255 -> T331,\nT256 -> T332,\nT257 -> T333,\nT258 -> T334,\nX161 -> .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))),\nX162 -> .(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 144 [arrowhead = none ];
144 -> 68;

145 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 145 [arrowhead = none ];
145 -> 69;

146 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 146 [arrowhead = none ];
146 -> 67;

147 [label="GENERALIZATION\nT351 <-- .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, [])))))))\nT352 <-- .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))\n\nNew Knowledge:\nT351 is ground\nT352 is ground", fontsize=14, style = filled, fillcolor = violet];
68 -> 147 [arrowhead = none ];
147 -> 70;

148 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
70 -> 148 [arrowhead = none ];
148 -> 71;

149 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
71 -> 149 [arrowhead = none ];
149 -> 72;

150 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
71 -> 150 [arrowhead = none ];
150 -> 73;

151 [label="EVAL with clause\nreverse([], X171, X171).\nand substitutionT327 -> [],\nT326 -> T365,\nT351 -> T366,\nX171 -> .(T365, T366),\nT334 -> T365,\nT352 -> T366", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 151 [arrowhead = none ];
151 -> 74;

152 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 152 [arrowhead = none ];
152 -> 75;

153 [label="EVAL with clause\nreverse(.(X180, X181), X182, X183) :- reverse(X181, .(X180, X182), X183).\nand substitutionX180 -> T379,\nX181 -> T380,\nT327 -> .(T379, T380),\nT326 -> T381,\nT351 -> T382,\nX182 -> .(T381, T382),\nT334 -> T383,\nT352 -> T384,\nX183 -> .(T383, T384)", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 153 [arrowhead = none ];
153 -> 77;

154 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 154 [arrowhead = none ];
154 -> 78;

155 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 155 [arrowhead = none ];
155 -> 76;

156 [label="INSTANCE with matching:\nT327 -> T380\nT326 -> T379\nT351 -> .(T381, T382)\nT334 -> T383\nT352 -> T384", fontsize=14, style = filled, fillcolor = lightgrey];
77 -> 156 [arrowhead = none , style=dashed];
156 -> 70[style=dashed];

}

(2) Obligation:

Triples:

reverseA(.(X1, X2), X3, X4, X5, X6) :- reverseA(X2, X1, .(X3, X4), X5, X6).
palindromeB(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) :- reverseA(X9, X8, .(X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, []))))))), X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))).

Clauses:

reversecA([], X1, X2, X1, X2).
reversecA(.(X1, X2), X3, X4, X5, X6) :- reversecA(X2, X1, .(X3, X4), X5, X6).

Afs:

palindromeB(x1)  =  palindromeB(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
palindromeB_in: (b)
reverseA_in: (b,b,b,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

PALINDROMEB_IN_G(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → U2_G(X1, X2, X3, X4, X5, X6, X7, X8, X9, reverseA_in_ggggg(X9, X8, .(X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, []))))))), X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
PALINDROMEB_IN_G(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → REVERSEA_IN_GGGGG(X9, X8, .(X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, []))))))), X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))
REVERSEA_IN_GGGGG(.(X1, X2), X3, X4, X5, X6) → U1_GGGGG(X1, X2, X3, X4, X5, X6, reverseA_in_ggggg(X2, X1, .(X3, X4), X5, X6))
REVERSEA_IN_GGGGG(.(X1, X2), X3, X4, X5, X6) → REVERSEA_IN_GGGGG(X2, X1, .(X3, X4), X5, X6)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PALINDROMEB_IN_G(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → U2_G(X1, X2, X3, X4, X5, X6, X7, X8, X9, reverseA_in_ggggg(X9, X8, .(X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, []))))))), X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
PALINDROMEB_IN_G(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → REVERSEA_IN_GGGGG(X9, X8, .(X7, .(X6, .(X5, .(X4, .(X3, .(X2, .(X1, []))))))), X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))
REVERSEA_IN_GGGGG(.(X1, X2), X3, X4, X5, X6) → U1_GGGGG(X1, X2, X3, X4, X5, X6, reverseA_in_ggggg(X2, X1, .(X3, X4), X5, X6))
REVERSEA_IN_GGGGG(.(X1, X2), X3, X4, X5, X6) → REVERSEA_IN_GGGGG(X2, X1, .(X3, X4), X5, X6)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REVERSEA_IN_GGGGG(.(X1, X2), X3, X4, X5, X6) → REVERSEA_IN_GGGGG(X2, X1, .(X3, X4), X5, X6)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(7) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REVERSEA_IN_GGGGG(.(X1, X2), X3, X4, X5, X6) → REVERSEA_IN_GGGGG(X2, X1, .(X3, X4), X5, X6)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(9) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• REVERSEA_IN_GGGGG(.(X1, X2), X3, X4, X5, X6) → REVERSEA_IN_GGGGG(X2, X1, .(X3, X4), X5, X6)
  The graph contains the following edges 1 > 1, 1 > 2, 4 >= 4, 5 >= 5

(10) YES